\begin{tabbing}
$\forall$\=$A$:Type, ${\it eq}$:EqDecider($A$), $B$, $C$, $D$, $E$, $F$, $G$:($A$$\rightarrow$Type), $f$:$a$:$A$ fp$\rightarrow$ $B$($a$), $g$:$a$:$A$ fp$\rightarrow$ $C$($a$),\+
\\[0ex]$h$:$a$:$A$ fp$\rightarrow$ $D$($a$).
\-\\[0ex]($\forall$$a$:$A$. $B$($a$) $\subseteq\rho$ $E$($a$))
\\[0ex]$\Rightarrow$ ($\forall$$a$:$A$. $C$($a$) $\subseteq\rho$ $F$($a$))
\\[0ex]$\Rightarrow$ ($\forall$$a$:$A$. $D$($a$) $\subseteq\rho$ $E$($a$))
\\[0ex]$\Rightarrow$ ($\forall$$a$:$A$. $D$($a$) $\subseteq\rho$ $F$($a$))
\\[0ex]$\Rightarrow$ ($\forall$$a$:$A$. $F$($a$) $\subseteq\rho$ $G$($a$))
\\[0ex]$\Rightarrow$ ($\forall$$a$:$A$. $E$($a$) $\subseteq\rho$ $G$($a$))
\\[0ex]$\Rightarrow$ \{$f$ $\parallel$ $h$ $\Rightarrow$ $g$ $\parallel$ $h$ $\Rightarrow$ $f$ $\oplus$ $g$ $\parallel$ $h$\}
\end{tabbing}